*****ASSUME ∀W.T(P,W);

1 ∀W.T(P,W)  (1)

*****∀E ↑ W1;

2 T(P,W1)  (1)

***** 2;

3 A(FOOL,W,W1)⊃T(P,W1)  (1)

*****∀I ↑ W1;

4 ∀W1.(A(FOOL,W,W1)⊃T(P,W1))  (1)

*****∀E KNOW FOOL,P,W;

5 T(K(FOOL,P),W)≡∀W1.(A(FOOL,W,W1)⊃T(P,W1))  

***** 4:5;

6 T(K(FOOL,P),W)  (1)

*****∀I ↑ W;

7 ∀W.T(K(FOOL,P),W)  (1)

*****⊃I 1⊃↑;

8 ∀W.T(P,W)⊃∀W.T(K(FOOL,P),W)  

*****ASSUME ∀W.T(K(FOOL,P),W);

9 ∀W.T(K(FOOL,P),W)  (9)

*****∀E ↑ W;

10 T(K(FOOL,P),W)  (9)

***** 5,10;

11 ∀W1.(A(FOOL,W,W1)⊃T(P,W1))  (9)

*****∀E ↑ W;

12 A(FOOL,W,W)⊃T(P,W)  (9)

*****∀E REFLEX FOOL,W;

13 A(FOOL,W,W)  

***** 12:13;

14 T(P,W)  (9)

*****∀I ↑ W;

15 ∀W.T(P,W)  (9)

*****⊃I 9⊃↑;

16 ∀W.T(K(FOOL,P),W)⊃∀W.T(P,W)  

***** 8,16;

17 ∀W.T(P,W)≡∀W.T(K(FOOL,P),W)  

*****∀I ↑ P;

18 ∀P.(∀W.T(P,W)≡∀W.T(K(FOOL,P),W))